;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
;(require "Ilist.lisp")
;(require "Itrim.lisp")
;(require "Imerge-sort.lisp")
;(require "Iformulas-aux.lisp")
;(require "Ischedule-criterion.lisp")
;(require "Igpa-criterion.lisp")
;(require "Igender-criterion.lisp")
;(require "Iskill-sets-criterion.lisp")
;(require "Iformulas.lisp")
;(require "Irng.lisp")
(require "Idriver.lisp")
(require "IAVLtree.lisp")
(require "IcommonTimes.lisp")

(module Mdriver-private

;  (import Ilist)
;  (import Itrim)
;  (import Imerge-sort)
;  (import Iformulas-aux)
;  (import Ischedule-criterion)
;  (import Igpa-criterion)
;  (import Igender-criterion)
;  (import Iskill-sets-criterion)
;  (import Iformulas)
;  (import Irng)
  (import IAVLtree)
  (import IcommonTimes)
  
  (include-book "io-utilities" :dir :teachpacks)
  (include-book "list-utilities" :dir :teachpacks)
  (include-book "rand" :dir :teachpacks)
  
  
  (defconst *K* 48)
  (defconst *MIN-GPA* 2)
  (defconst *MAX-GPA* 4)
  (defconst *GPA-GAP/2* 0.125)
  (defconst *CONVERTED-GRADE-LENGTH*
    (/ (- *MAX-GPA* *MIN-GPA*) (* *GPA-GAP/2* 2)))

  (defconst *FEMALE* "f")
  (defconst *MALE* "m")
  (defconst *GENDER-LIST* (list *FEMALE* *MALE*))
  (defconst *UPPER-BOUND-FOR-LOW-GENDER-PERCENTAGE* 0.33)
  (defconst *NO-SUFFICIENT-LOW-PERCENTAGE-GENDER* "N/A")

  (defconst *NO-SUB-WEIGHT-INPUT* "NO SUB-WEIGHT INPUT")

  (defconst *INVALID-INPUT-SPECIFICATION-LINE*
    "INVALID INPUT IN SPECIFICATION LINE!")
  (defconst *INVALID-GENDER-INPUT*
  "INVALID GENDER INPUT!")
  
  (defconst *UNKNOWN-ERROR* "UNKNOWN ERROR!!!")
  (defconst *SKILL-SET* "SKILL SET")
  
  #|--------------------------------------------
  Itrim
----------------------------------------------|#
(defund trim-aux (x)
    (declare (xargs :guard (character-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp x)
        (if (or (eql (car x) #\Space)
                (eql (car x) #\Tab)
                (eql (car x) #\Newline)
                (eql (car x) #\Page))
            (trim-aux (cdr x))
          x)
      nil))

(defthm character-listp-of-trim-aux
  (implies (force (character-listp x))
           (character-listp (trim-aux x)))
  :hints(("Goal" :in-theory (enable trim-aux))))

(defthm true-listp-when-character-listp
         (implies (character-listp x)
                  (true-listp x)))

(defund trim (x)
    (declare (xargs :guard (stringp x)))
    (let* ((chars (coerce x 'list))
           (chars (trim-aux chars)) ;; eat spaces at the front
           (chars (reverse chars))  ;; flip so we can get to the back
           (chars (trim-aux chars)) ;; eat spaces at the back
           (chars (reverse chars))) ;; flip again so it's back to normal
      (coerce chars 'string)))

(defun trim-list-of-strs (strs)
   (declare (xargs :guard (string-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp strs)
        (cons (trim (car strs))
              (trim-list-of-strs (cdr strs)))
        nil))
#| -------------------------------------------|#
  
  (defun get-total-weight (list-of-input-weights)
  (if (rational-listp list-of-input-weights)
      (if (consp list-of-input-weights)
          (+ (abs (car list-of-input-weights))
             (get-total-weight (cdr list-of-input-weights)))
          0)
      list-of-input-weights))

(defun get-list-of-actual-weights
  (list-of-input-weights total-weight)
  (if (posp total-weight)
      (if (consp list-of-input-weights)
          (cons (/ (car list-of-input-weights)
                   total-weight)
                (get-list-of-actual-weights (cdr list-of-input-weights)
                                            total-weight))
          nil)
      list-of-input-weights))

(defun get-considered-skill-sets-as-strs
  (skill-set-specification-str-down-case)
  (map-chrs->str (remove nil (packets #\; (str->chrs 
                                           skill-set-specification-str-down-case)))))

(defun digit-chars-p
  (chrs)
  (if (consp chrs)
      (and (digit-char-p (car chrs))
           (digit-chars-p (cdr chrs)))
      t))

(defun get-input-considered-skill-sets
  (considered-skill-sets-as-strs)
  (if (consp considered-skill-sets-as-strs)
      (let* ((first-considered-skill-set-str
              (car considered-skill-sets-as-strs))
             (user-did-input-skill-set-name
              (member-equal #\: (str->chrs first-considered-skill-set-str)))
             (first-considered-skill-set-data
              (map-chrs->str (remove nil (packets #\, (str->chrs first-considered-skill-set-str)))))
             (first-ele-in-first-considered-skill-set-data
              (car first-considered-skill-set-data))
             (rest-considered-skill-sets
              (get-input-considered-skill-sets (cdr considered-skill-sets-as-strs))))
        (if first-ele-in-first-considered-skill-set-data
            (let* (
             (user-did-input-sub-weight
              (digit-chars-p (str->chrs (trim first-ele-in-first-considered-skill-set-data)))))
        (cond 
          ((and user-did-input-sub-weight
                user-did-input-skill-set-name)
           (let* ((first-considered-skill-set-sub-weight
                   (str->rat first-ele-in-first-considered-skill-set-data))
                  (first-considered-skill-set-name-and-first-skill
                    (map-chrs->str
                     (remove nil
                             (packets #\:
                                      (str->chrs (cadr first-considered-skill-set-data))))))
                  (first-ele-in-first-considered-skill-set-name-and-first-skill
                   (car first-considered-skill-set-name-and-first-skill))
                  (first-considered-skill-set-name
                   (if first-ele-in-first-considered-skill-set-name-and-first-skill
                       (trim first-ele-in-first-considered-skill-set-name-and-first-skill)
                       *SKILL-SET*))
                  (second-ele-in-first-considered-skill-set-name-and-first-skill
                   (cadr first-considered-skill-set-name-and-first-skill))
                  (first-considered-skill-set-data-but-first-two
                   (cddr first-considered-skill-set-data))
                  (first-considered-skill-set
                   (cond
                     ((and second-ele-in-first-considered-skill-set-name-and-first-skill
                           first-considered-skill-set-data-but-first-two)
                      (trim-list-of-strs 
                       (cons second-ele-in-first-considered-skill-set-name-and-first-skill
                             first-considered-skill-set-data-but-first-two)))
                     ((and second-ele-in-first-considered-skill-set-name-and-first-skill
                           (not first-considered-skill-set-data-but-first-two))
                      (list (trim second-ele-in-first-considered-skill-set-name-and-first-skill)))
                     ((and (not second-ele-in-first-considered-skill-set-name-and-first-skill)
                           first-considered-skill-set-data-but-first-two)
                      (trim-list-of-strs first-considered-skill-set-data-but-first-two)))))
             (if first-considered-skill-set
                 (cons (list first-considered-skill-set-name
                             first-considered-skill-set-sub-weight
                             first-considered-skill-set)
                       rest-considered-skill-sets)
                 rest-considered-skill-sets)))
          
         ((and user-did-input-sub-weight
               (not user-did-input-skill-set-name))
          (let* ((first-considered-skill-set-sub-weight-no-name
                  (str->rat first-ele-in-first-considered-skill-set-data))
                 (first-considered-skill-set-no-name
                  (trim-list-of-strs (cdr first-considered-skill-set-data))))
            (if first-considered-skill-set-no-name
                (cons (list *SKILL-SET*
                             first-considered-skill-set-sub-weight-no-name
                             first-considered-skill-set-no-name)
                       rest-considered-skill-sets)
                 rest-considered-skill-sets)))
         
         ((and (not user-did-input-sub-weight)
               user-did-input-skill-set-name)
          (let* ((first-considered-skill-set-name-and-first-skill-no-weight
                  (map-chrs->str
                   (remove nil
                           (packets #\:
                           (str->chrs first-ele-in-first-considered-skill-set-data)))))
                  (first-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                   (car first-considered-skill-set-name-and-first-skill-no-weight))
                  (first-considered-skill-set-name-no-weight
                   (if first-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                       (trim first-ele-in-first-considered-skill-set-name-and-first-skill-no-weight)
                       *SKILL-SET*))
                  (second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                   (cadr first-considered-skill-set-name-and-first-skill-no-weight))
                  (first-considered-skill-set-data-but-first
                   (cdr first-considered-skill-set-data))
                  (first-considered-skill-set-no-weight
                   (cond
                     ((and second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                           first-considered-skill-set-data-but-first)
                      (trim-list-of-strs (cons second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                                               first-considered-skill-set-data-but-first)))
                     ((and second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight
                           (not first-considered-skill-set-data-but-first))
                      (list (trim second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight)))
                     ((and (not second-ele-in-first-considered-skill-set-name-and-first-skill-no-weight)
                           first-considered-skill-set-data-but-first)
                      (trim-list-of-strs first-considered-skill-set-data-but-first)))))
             (if first-considered-skill-set-no-weight
                 (cons (list first-considered-skill-set-name-no-weight
                             *NO-SUB-WEIGHT-INPUT*
                             first-considered-skill-set-no-weight)
                       rest-considered-skill-sets)
                 rest-considered-skill-sets)))
         (t
          (cons (list *SKILL-SET*
                      *NO-SUB-WEIGHT-INPUT*
                      (trim-list-of-strs first-considered-skill-set-data))
                rest-considered-skill-sets))))
            rest-considered-skill-sets))
      considered-skill-sets-as-strs))

(defun set-default-sub-weights-for-skill-sets
  (input-sub-weights-of-skill-sets)
  (if (consp input-sub-weights-of-skill-sets)
      (let ((first-input-sub-weight
             (car input-sub-weights-of-skill-sets))
            (rest-default-sub-weights
             (set-default-sub-weights-for-skill-sets
              (cdr input-sub-weights-of-skill-sets))))
        (if (or (equal first-input-sub-weight
                       *NO-SUB-WEIGHT-INPUT*)
                (= first-input-sub-weight 0))
            rest-default-sub-weights
            (cons first-input-sub-weight
                  rest-default-sub-weights)))
      nil))

(defun get-actual-sub-weights-of-skill-sets
  (input-sub-weights-of-skill-sets)
  (if (consp input-sub-weights-of-skill-sets)
      (let ((num-skill-sets
             (len input-sub-weights-of-skill-sets)))
        (if (not (drop-set (list *NO-SUB-WEIGHT-INPUT*)
                           input-sub-weights-of-skill-sets))
            (replicate num-skill-sets
                       (/ 1 num-skill-sets))
            (let ((default-sub-weights-for-skill-sets
                    (set-default-sub-weights-for-skill-sets
                     input-sub-weights-of-skill-sets)))
              (get-list-of-actual-weights default-sub-weights-for-skill-sets
                                          (get-total-weight
                                           default-sub-weights-for-skill-sets)))))
      nil))

(defun pairs (xs ys zs)
  (if (and (consp xs) (consp ys) (consp zs))
      (cons (list (car xs) (car ys) (car zs))
            (pairs (cdr xs) (cdr ys) (cdr zs)))
      nil))

(defun get-converted-skill-set-specifications
  (input-skill-sets)
  (if (consp input-skill-sets)
      (let* ((skill-set-names
             (strip-cars input-skill-sets))
             (input-sub-weights-of-skill-sets
              (strip-cars (strip-cdrs input-skill-sets)))
             (actual-sub-weights-of-skill-sets
              (get-actual-sub-weights-of-skill-sets input-sub-weights-of-skill-sets))
             (skill-sets
              (strip-cars (strip-cdrs (strip-cdrs input-skill-sets)))))
        (pairs skill-set-names
               actual-sub-weights-of-skill-sets
               skill-sets))
      nil))

  ;; converts a list of strings to a list of rational numbers
  (defun strs->rats (strs)
    (if (consp strs)
        (cons (str->rat (car strs)) (strs->rats (cdr strs)))
        nil))
  
  
  (defun getstrings (lines)
    (if (consp lines)
        (cons (chrs->str (car lines)) (getstrings (cdr lines)))
        nil
        )
    )
  
  (defun my-loc-from-file-as-string (str)
    (packets #\Newline (str->chrs str)))
  
  (defun my-loc (file-path state)
    (mv-let (str error state)
            (file->string file-path state)
            (if error
                (mv error state)
                (mv (getstrings (my-loc-from-file-as-string str)) state))))
  
 
  
  ; Main function for getting a student's schedule as a bit array
  ; initializes the array, packets the student's string and removes
  ; spaces
  (defun schedule-as-bit-array-from-student-as-str (student-as-string)
    (timeString->bitList (chrs->str (cadr (cddddr (packets #\| (str->chrs student-as-string))))))
  )
  
  ; Takes in a filename and outputs its contents as a string
  (defun get-input-file-as-str (input)
    (mv-let (file-as-string error state)
            (file->string input state)
            (map-chrs->str 
             (remove nil (packets-set (list (code-char 10) (code-char 13)) (str->chrs file-as-string))))
            )
    )
  
  ; Takes in a student as a string and converts it into 
  ; usuable data
  ; The format is:
  ; ( "ID" "FirstName LastName" "Gender" "Grade" "Skillsets" (0 0 0 1 0 1 1 1 ...))
  ; Where the bit array is the student's schedule
  (defun student-to-data (student)
    (let ((student-packet (packets #\| (str->chrs student))))
      (if (or (equal (remove #\space (caddr student-packet)) (list #\M)) 
              (equal (remove #\space (caddr student-packet)) (list #\m)))
          (list (chrs->str (car student-packet))  (chrs->str (cadr student-packet)) "m" 
                (str->rat (chrs->str (cadddr student-packet)))
                (string-downcase (chrs->str (car (cddddr student-packet))))
                (schedule-as-bit-array-from-student-as-str student))
          (list (chrs->str (car student-packet))  (chrs->str (cadr student-packet)) "f" 
                (str->rat (chrs->str (cadddr student-packet))) 
                (string-downcase (chrs->str (car (cddddr student-packet))))
                (schedule-as-bit-array-from-student-as-str student))
      )
    )
  )
  
  ; Cycles through the list of students and turns them into usable data
  (defun get-students-as-data-helper (students)
    (if (consp students)
        (cons (student-to-data (car students)) 
              (get-students-as-data-helper (cdr students)))
        nil
        )
    )
  
  ; Main function for student-strings into data, input is the filename
  (defun get-students-as-data (input)
    (get-students-as-data-helper (cdr (get-input-file-as-str input)))
    )
  
  ;gets rid of extra spaces and punctuation between words 
  (defun strs-join (glue strs)
    (if(endp strs)
       ""
       (if (endp (cdr strs))
           (car strs)
           (concatenate 'string
                        (car strs)
                        glue
                        (strs-join glue (cdr strs)))
           )))
  
  ;gets ride of white space thatis in a single string 
  (defun trim-stringss (ss)
    (if (endp ss) ss
        (cons 
         (strs-join " " (words (car ss))) 
         (trim-stringss (cdr ss)))))
  
  (defun str->rat-caar (tr)
    (cons (cons (str->rat(car (car tr)))
                (cdr (car tr)))
          (cdr tr)))
  
  ;gets the five numbers at the begining of the specification line (#teams & weights) 
  ;packets remainder of string by semi-colon 
  (defun input-parse-helper (xs)
    (if (equal (len xs) 6)
    (cons (strs->rats (trim-stringss (take 5 xs)))
         (car (nthcdr 5 xs)))
    "Error!"))
  
  ;packets the string at |  
  (defun parse-input (file-path)
    (input-parse-helper 
              (getstrings (packets #\| (str->chrs (car (get-input-file-as-str file-path))))))
  )
  
  ;gets number of teams user wants to have
  (defun get-num-teams (xs)
    (caar xs)
    )
  
  (defun get-sum-of-weights (weights acc)
    (if (consp weights)
        (get-sum-of-weights (cdr weights) (+ (car weights) acc))
        acc
    )
  )
  
  (defun get-weights  (xs)
    (let ((sum-of-weights (get-sum-of-weights (cdar xs) 0)))
      (list (/ (cadar xs) sum-of-weights) (/ (caddar xs) sum-of-weights)
            (/ (car (cdddar xs)) sum-of-weights) (/ (cadr (cdddar xs)) sum-of-weights))
    )
  ) 

  ;gets all skill 
  (defun get-skill-sets (xs)
    (cdr(car xs))
    )
  
  
  (defun rats->str(nums)
    (if (consp nums)
        (concatenate 'string (rat->str (car nums) 0) (rats->str (cdr nums)))
         ""))
  
  ; Returns each member's ID and name
  (defun member-output (members)
    (if (consp members)
        (concatenate 'string 
                     (nth 0 (car members))"    " 
                     (nth 1 (car members))"    " 
                     ;(nth 2 (car members))"    "
                     ;(rat->str (nth 3 (car members)) 1)"    "
                     ;(nth 4 (car members))"    "
                     ;(rats->str (nth 5 (car members)))"    "
                     "\n\t\t" (member-output (cdr members)))
        ""
    )
  )
  
  
  ; Runs through each group and passes its members to member-output
  (defun output-helper (group)
    (concatenate 'string 
                 "Group " (int->str (+ 1(caar group)))
                 "    Score: " (rat->str (cadar group) 3)
                 "    Common Times: " (bitlist->timesstring (get-common-times-output (cdr group))) ; Calls the McommonTimes module
                 "\n\t\t" (member-output (cdr group)) "\n\t")
  )
  
  ; Main output function, given a flattened avl tree (with flattened avl tree data)
  ; it returns a string to write to a file
  (defun output-groups (flattened-tree)
    (if (consp flattened-tree)
        (string-append (output-helper (car flattened-tree)) (output-groups (cdr flattened-tree)))
        ""
    )
  )
  
  ; Returns a string of the output
  (defun output (specs flattened-tree)
    (let ((sum-of-weights (get-sum-of-weights (get-weights specs) 0))
          (weights (get-weights specs)))
         (concatenate 'string "Team Set Criteria:\n\tGrade (" (rat->str (/ (car weights) sum-of-weights) 3) 
                      ")\n\tSkill sets (" (rat->str (/ (cadddr weights) sum-of-weights) 3) ")\n\tSchedule ("
                      (rat->str (/ (cadr weights) sum-of-weights) 3) ")\n\tGender (" 
                      (rat->str (/ (caddr weights) sum-of-weights) 3) ")\n\nSuggested Team Set:\n\t" 
                      (output-groups flattened-tree))
    )
  )
  
  ; Gets the appropriate seed
  (defun ith-seed (seed i)
    (if (equal i 0)
        seed
        (ith-seed (next-seed seed) (- i 1))
        )
    )
  
  ; Iterates 50 fifty times to find the best tree
  (defun iterate-trees (students num-teams weights specifications seed i current-best-tree)
    (if (< i 50)
        (let* ((current-tree 
                (form-initial-tree students num-teams weights specifications (ith-seed seed i))))
          (if (> (cadaar current-tree) (cadaar current-best-tree))
              (iterate-trees students num-teams weights specifications seed (+ i 1) current-tree)
              (iterate-trees students num-teams weights specifications seed (+ i 1) current-best-tree)
              )
          )
        current-best-tree
        )
    )
  
  ;takes in the input file and writes out the output file
  (defun team-creator (input-file output-file) 
    (let ((specs (parse-input input-file)))
      (if (not (stringp specs))
        (string-list->file output-file (list (output specs 
                                                       (iterate-trees 
                                        (get-students-as-data input-file) 
                                         (get-num-teams specs) (get-weights specs)
                                         (get-converted-skill-set-specifications (get-input-considered-skill-sets (get-considered-skill-sets-as-strs
                                                          (string-downcase (cdr specs))))) (initial-seed) 0
                                         (form-initial-tree (get-students-as-data input-file) 
                                                          (get-num-teams specs) (get-weights specs) 
                                                          (get-converted-skill-set-specifications (get-input-considered-skill-sets (get-considered-skill-sets-as-strs
                                                          (string-downcase (cdr specs))))) (initial-seed))
                                         )
                                                    )) 
                             state)
           specs
      )
    )
  )
  
  (export Idriver)
)

(link Mdriver
  (import ;Ilist Itrim Imerge-sort Iformulas-aux Ischedule-criterion Igpa-criterion
          ;Igender-criterion Iskill-sets-criterion Iformulas Irng 
   IAVLtree IcommonTimes)
  (export Idriver)
  (Mdriver-private))
